Subject: KIF Re: the Heraclitus distinction metatheory
Date: Wed, 6 Dec 2000 16:49:53 -0800
From:  "Robert E. Kent" <rekent@ontologos.org>
To:"SUO" <standard-upper-ontology@ieee.org>
References: 1




All,

The sorted version of the theory of the Heraclitus distinction may be seen
as a little clearer than the unsorted (one-sorted) version. Here there are
three sorts of things: entities, individuals and classes. Let us denote the
sorts by $ent, $ind and $cls, respectively.

    SUO[$ent] denotes the ENTITY metaclass
    SUO[$ind] denotes the INDIVIDUAL metaclass
    SUO[$cls] denotes the CLASS metaclass

So we do not need the corresponding 1-place metapredicate symbols.

Sequent constraints on sorts are specified as follows.

    [necessity:]   |- $ent
    [subtype:]   $ind |- $ent   and   $cls |- $ent
    [disjointness:]   $ind, $cls |-
    [covering:]   $ent |- $ind, $cls

This automatically induces the required partition

    SUO[*] = SUO[$ent] = SUO[$ind] + SUO[$cls]

Finally, the sort of the INSTANCE-OF metapredicate symbol is specified as
follows.

    sort[INSTANCE-OF] = <$ent, $cls>

This automatically induces the required typing

    SUO[INSTANCE-OF] \subset SUO[$ent] x SUO[$cls]

No axioms are necessary.

Robert E. Kent
rekent@ontologos.org

----- Original Message -----
From: "Robert E. Kent" <rekent@ontologos.org>
To: "SUO-KIF" <suo-kif@ieee.org>; "SUO" <standard-upper-ontology@ieee.org>
Sent: Tuesday, December 05, 2000 4:12 PM
Subject: SUO: the Heraclitus distinction metatheory


> All,
>
> Attached is the SUO-KIF metatheory of the Heraclitus distinction conceived
> as a formal context.
>
> Robert E. Kent
> rekent@ontologos.org
>





;; A metalevel KIF encoding of the Heraclitus distinction,
;; as discussed in the messages
;; [http://ltsc.ieee.org/logs/suo/msg02424.html]
;; [http://ltsc.ieee.org/logs/suo/msg02422.html] and
;; [http://ltsc.ieee.org/logs/suo/msg02351.html].
;; The three sections -- World, Model and Theory -- are divided
;; according to the triptych indicated in the image
;; [http://www.bestweb.net/~sowa/ontology/mthworld.gif].

;;;;;;;;;;;;;;;;;;;;
;; WORLD
;;;;;;;;;;;;;;;;;;;;

;; DISCUSSION: The Heraclitus Ontological Atom

;; This ontological atom models the meaning of the Heraclitus 
;; distinction, which may lay at the heart of the structure of the 
;; SUO. This core structure is in the form of the Heraclitus formal 
;; context (the mathematical context from Formal Concept Analysis)
;;
;;	Heraclitis = (ENTITY, CLASS, INSTANCE-OF),
;;
;; where the metaclass ENTITY, the "domain" or "universe of discourse"
;; consisting of any non-relational thing (relations get in
;; second-hand by reification or hypostatic abstraction 
;; [http://www.clas.ufl.edu/users/jzeman/peirce_on_abstraction.htm]),
;; is the disjoint union
;;
;;	ENTITY = INDIVIDUAL + CLASS.
;;
;; This representation of the Heraclitus distinction is somewhat
;; different from that used in John Sowa's book "Knowledge
;; Representation." It follows Aristotle, who set out two tasks for
;; the philosopher (see the Encyclopedia Britannica article
;; [http://www.britannica.com/bcom/eb/article/3/0,5716,115523+1+108718,00.html?query=metaphysics])
;;
;;	[second philosophy:] to investigate the nature and properties
;;	of what exists in the natural, or sensible, world.
;;
;;	[first philosophy:] to explore the characteristics of "Being
;;	as such" and to inquire into the character of "the substance
;;	that is free from movement," or the most real of all things,
;;	the intelligible reality on which everything in the world of
;;	nature was thought to be causally dependent. 
;;
;; Heraclitus's Logos corresponds quite closely to Plato's Form
;; (noumena, object of intelligence) and Aristotle's Category, or
;; what we are calling the metaclass Class in the SUO.
;; 
;; Heraclitus's Physis translates as something natural or growing
;; and corresponds to Plato's Phenomena and the objects of nature
;; studied in Aristotle's second philosophy. Since, in one sense,
;; in SUO the dual of CLASS is the metaclass INDIVIDUAL, here this
;; is made the correspondent to Physis.
;;
;; See the table of correspondences at
;; [http://ltsc.ieee.org/logs/suo/doc00000.doc].
;;
;; Note: a class can appear in the Heraclitus formal context as
;; either a "formal object" (1st argument of INSTANCE-OF) or a
;; "formal attribute" (2nd argument of INSTANCE-OF).
;; 
;; For example, if the term "Triangle" denotes the class of triangles,
;;
;;	(CLASS Triangle)
;;
;; then the triangle "Triangle#123" that I have drawn on my paper
;;
;;	(INDIVIDUAL Triangle#123)
;;
;; and the shape "Shape#345" of the flat iron building in New York
;;
;;	(INDIVIDUAL Shape#345)
;;
;; are two instances of "Triangle"
;;
;;	(INSTANCE-OF Triangle#123 Triangle)
;;	(INSTANCE-OF Shape#345 Triangle)
;;
;; whereas the class "Triangle" is an instance of the higher-order
;; class "GeometricShape"
;;
;;	(CLASS GeometricShape)
;;	(INSTANCE-OF Triangle GeometricShape).


;;;;;;;;;;;;;;;;;;;;
;; MODEL
;;;;;;;;;;;;;;;;;;;;

;; DISCUSSION

;; A 1st-order model for unsorted (one-sorted) SUO-KIF should have
;; a domain or universe of discourse SUO[*], where "*" is the only
;; sort, and an interpretation for all metapredicate symbols p and
;; metaconstants c -- let these be denoted SUO[p] and SUO[c]. The
;; interpretations should satisfy the constraints: 
;;
;;	SUO[c] \member SUO[*]
;;	SUO[p] \subset SUO[*]^n
;;
;; for all predicate symbols p with valence n.

;; LANGUAGE

;; In the Heraclitus distinction metatheory, the lexicon consists
;; only of the four primitive metapredicates
;;
;; 1-place: ENTITY, INDIVIDUAL, CLASS
;; 2-place: INSTANCE-OF

;; SEMANTIC CONSTRAINTS

;; From the above discussion, the interpretation should satisfy the
;; following constraints:
;;
;;	SUO[*] = SUO[ENTITY]
;;	       = SUO[INDIVIDUAL] + SUO[CLASS]
;;
;;	For any two things X and Y,
;;		if (X, Y) is in SUO[INSTANCE-OF],
;;		then SUO[X] is in SUO[ENTITY] and SUO[Y] is in SUO[CLASS]. 


;;;;;;;;;;;;;;;;;;;;
;; THEORY
;;;;;;;;;;;;;;;;;;;;

;; LANGUAGE

(documentation ENTITY "Everything that is not a predicate, or the top metaclass.")

(documentation INDIVIDUAL "The universe of discourse, or metaclass of individual entities.")

(documentation CLASS "All type-like entities, or the metaclass of classes.")

(documentation INSTANCE-OF "The basic incidence between entities and classes.")

;; AXIOMS

(documentation "AXIOM: Everything is an entity.")

(forall (?x)(ENTITY ?x))

(documentation "AXIOM: Every entity is either an individual or a class, but not both.")

(forall (?x)
        (or (INDIVIDUAL ?x) (CLASS ?x))
        (not (and (INDIVIDUAL ?x) (CLASS ?x)))
)

(documentation "AXIOM: All entities can be instances of classes, but only classes can have instances.")

(forall (?x ?y)
        (=> (INSTANCE-OF (?x ?y))
            (and (ENTITY ?x) (CLASS ?y))
        )
)